with decls ds dasends on l from e include f(e) and only these for tags in tgs
== (e:es-E(es). 
== (es-isrcv(es; e))
==  (es-lnk(es; e) = l)
==  (e':es-E(es)
==  (((es-isrcv(es; e'))
==  (c ((es-lnk(es; e') = l)
==  (c  (es-tag(es; e')  tgs)
==  (c  (es-sender(es; e') = es-sender(es; e)))))
==  (es-tag(es; e)  tgs))
== c ((e':es-E(es). 
== c (es-isrcv(es; e'))
== c  (es-lnk(es; e') = l)
== c  (es-tag(es; e')  tgs)
== c  subtype_rel(es-valtype(es; e'); fpf-cap(da; Kind-deq; es-kind(es; e'); void)))
== c  (x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top))))
== c (alle-at(es;
== c (alle-at(source(l);
== c (alle-at(e.(i:int_seg(0; ||f(e)||). 
== c (alle-at(e':es-E(es)
== c (alle-at(((es-isrcv(es; e'))
== c (alle-at( (es-lnk(es; e') = l)
== c (alle-at( (es-tag(es; e')  tgs)
== c (alle-at( (es-sender(es; e') = e)
== c (alle-at( (es-index(es; e') = i))))
== c  (e':es-E(es). 
== c  (es-isrcv(es; e'))
== c   (es-lnk(es; e') = l)
== c   (es-tag(es; e')  tgs)
== c   ((es-index(es; e') < ||f(es-sender(es; e'))||)
== c   c (<es-tag(es; e'), es-val(es; e')> = f(es-sender(es; e'))[es-index(es; e')])))) 

latex

---

clarification:

es-sends-iff(es;l;tgs;da;ds;e.f(e))
== (e:es-E(es). 
== (es-isrcv(es; e))
==  (es-lnk(es; e) = l  IdLnk)
==  (e':es-E(es)
==  (((es-isrcv(es; e'))
==  (c ((es-lnk(es; e') = l  IdLnk)
==  (c  (es-tag(es; e')  tgs  Id)
==  (c  (es-sender(es; e') = es-sender(es; e)  es-E(es)))))
==  (es-tag(es; e)  tgs  Id))
== c ((e':es-E(es). 
== c (es-isrcv(es; e'))
== c  (es-lnk(es; e') = l  IdLnk)
== c  (es-tag(es; e')  tgs  Id)
== c  subtype_rel(es-valtype(es; e'); fpf-cap(da; Kind-deq; es-kind(es; e'); void)))
== c  (x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top))))
== c (alle-at(es;
== c (alle-at(source(l);
== c (alle-at(e.(i:int_seg(0; ||f(e)||). 
== c (alle-at(e':es-E(es)
== c (alle-at(((es-isrcv(es; e'))
== c (alle-at( (es-lnk(es; e') = l  IdLnk)
== c (alle-at( (es-tag(es; e')  tgs  Id)
== c (alle-at( (es-sender(es; e') = e  es-E(es))
== c (alle-at( (es-index(es; e') = i  ))))
== c  (e':es-E(es). 
== c  (es-isrcv(es; e'))
== c   (es-lnk(es; e') = l  IdLnk)
== c   (es-tag(es; e')  tgs  Id)
== c   ((es-index(es; e') < ||f(es-sender(es; e'))||)
== c   c (<es-tag(es; e'), es-val(es; e')>
== c   c (=
== c   c (f(es-sender(es; e'))[es-index(es; e')]
== c   c ( (tg:Id  fpf-cap(da; Kind-deq; rcv(l,tg); void)))))) 

latex

Definitions	es-valtype(es; e), es-kind(es; e), es-vartype(es; i; x), id-deq, top, alle-at(es; i; e.P(e)), source(l), int_seg(i; j), #$n, x:A. B(x), P  Q, , x:A. B(x), es-E(es), b, es-isrcv(es; e), IdLnk, es-lnk(es; e), P  Q, (x  l), A c B, a < b, ||as||, s = t, x:A  B(x), Id, fpf-cap(f; eq; x; z), Kind-deq, rcv(l,tg), void, <a, b>, es-tag(es; e), es-val(es; e), l[i], es-index(es; e), es-sender(es; e)
FDL editor aliases	es-sends-iff